| Definitions | x:A B(x), A & B, t  T, Realizer, f(a), {x:A| B(x) }, x:A  B(x),  x:A. B(x), P   Q, e@i. P(e), valtype(e), kind(e), locl(a), P & Q, P  Q, Void,  x:A. B(x), Top,  b,  A,  b,  , s = t, Prop, a = b, Unit, left+right, KindDeq, Knd,  x:A. B(x), Type, lnk-decl(l;dt), f(x)?z, x : v,  x.A(x), x. t(x), x dom(f), a:A fp B(a), Valtype(da;k), IdDeq, Id, vartype(i;x), S  T, f  g, left right, R-Feasible(R), R ||- es.P(es), {T}, SQType(T), s ~ t, Atom$n, a = b, S  T, E, loc(e), @i: only members of L read x, es realizer ind Rrframe compseq tag def, Consistent(R;es), @loc: only members of L read x, ES, R-da(R;i), State(ds), R-state(R;i), state@i, @i:k sends only on links in L, es realizer ind Rbframe compseq tag def, @loc: k sends only on links in L, @i: k affects only L, es realizer ind Raframe compseq tag def, @loc: k writes only members of L, , if b t else f fi, @i Precondition for a(v)P State(ds) (v:T), es realizer ind Rpre compseq tag def, @loc precondition for a(v:T):P State(ds) v, source(l), sends k(v:T) on l:tagged(g,State(ds),v):dt, es realizer ind Rsends compseq tag def, sends knd(v:T) on l:tagged(g,State(ds),v):dt, @i events of kind k change x to f State(ds) (val:T), es realizer ind Reffect compseq tag def, @loc effect knd(v:T) x := f State(ds) v , only events in L send on l with tg, es realizer ind Rsframe compseq tag def, only events in L send on lnk with tag, @i only events in L change x : T, es realizer ind Rframe compseq tag def, @loc only events in L change x:T, @i x initially v:T, es realizer ind Rinit compseq tag def, @loc x initially v:T, type List, IdLnk, DeclaredType(ds;x), x,y,z. t(x;y;z), x,y,z,w,v. t(x;y;z;w;v), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z,w. t(x;y;z;w), es realizer ind, es realizer ind Rplus compseq tag def, True, es realizer ind Rnone compseq tag def,  , rec(x.A(x)), Dec(P), P Q, x initially@i , tag(k), rcv(l,tg), tag(e), <a,b>, 1of(t), a = b, False, f(x), Case b of inl(x) s(x) ; inr(y) t(y) |
| Lemmas | lnk-decl-dom-not, lnk-decl-cap2, assert-eq-lnk, eq lnk wf, es-kind-rcv, fpf-single-dom, Knd sq, R-da wf, subtype rel dep function iff, decidable equal Id, es-initially wf, subtype rel dep function, subtype rel self, R-state wf, unit wf, Rnone wf, es realizer ind wf, es realizer wf, decl-type wf, decl-state wf, IdLnk wf, Rinit wf, Rframe wf, Rsframe wf, Reffect wf, Rsends wf, fpf-join wf, lsrc wf, Rpre wf, ma-valtype wf, ifthenelse wf, fpf wf, fpf-empty wf, Raframe wf, Rbframe wf, event system wf, R-consistent wf, Rrframe wf, es-loc wf, es-E wf, es-valtype wf, not functionality wrt iff, assert-eq-id, eq id wf, Id sq, R-Feasible wf, Rplus wf, es-vartype wf, fpf-cap wf, Id wf, id-deq wf, fpf-join-cap-sq, fpf-trivial-subtype-top, lnk-decl wf, fpf-dom wf, fpf-single wf, top wf, fpf-cap-single, Knd wf, Kind-deq wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, eq knd wf, bool wf, bnot wf, not wf, assert wf, assert-eq-knd, locl wf, es-kind wf |
State(R-state(A;i)) &